Iof proof for Lemma equiv rel functionality wrt iff:
1. T : Type
2. T' : Type
3. E : T
T
4. E' : T'
T'
5. T = T'
6.
x, y:T. E(x,y) 
E'(x,y)
7. EquivRel(
;A,B.A B)
((a:T. E'(a,a)) & (a, b:T. E'(a,b) E'(b,a)) & (a, b, c:T. E'(a,b) E'(b,c) E'(a,c)))
((a:T'. E'(a,a))
& (a, b:T'. E'(a,b) E'(b,a))
& (a, b, c:T'. E'(a,b) E'(b,c) E'(a,c)))
by RepUnfolds ``equiv_rel refl`` 7
1:
1: 7. (a:. a a) & Sym(;A,B.A B) & Trans(;A,B.A B)
1: ((a:T. E'(a,a))
1: & (a, b:T. E'(a,b) E'(b,a))
1: & (a, b, c:T. E'(a,b) E'(b,c) E'(a,c)))
1: ((a:T'. E'(a,a))
1: & (a, b:T'. E'(a,b) E'(b,a))
1: & (a, b, c:T'. E'(a,b) E'(b,c) E'(a,c)))
.